Left Termination proof of /tmp/tmp4sf

Left Termination of the query pattern transpose_aux(f,b,f) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

transpose_aux₃(.₂(R, Rs), underscore, .₂(C, Cs)) :- row2col₅(R, .₂(C, Cs), Cols1, {}₀, Accm).
row2col₅(.₂(X, Xs), .₂(.₂(X, Ys), Cols), .₂(Ys, Cols1), A, B) :- row2col₅(Xs, Cols, Cols1, .₂({}₀, A), B).

With regard to the inferred argument filtering the predicates were used in the following modes:
transpose_aux₃: (f,b,f)
row2col₅: (f,b,f,b,f) (f,f,f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGA₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_5_IN_AGAGA₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

The argument filtering Pi contains the following mapping:
transpose_aux_3_in_aga₃(x1, x2, x3) = transpose_aux_3_in_aga₁(x2)
._2₂(x1, x2) = ._2
[]_0 = []_0
if_transpose_aux_3_in_1_aga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_aga₁(x6)
row2col_5_in_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_in_aaaga₁(x4)
if_row2col_5_in_1_aaaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_aaaga₁(x8)
row2col_5_out_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_out_aaaga₄(x1, x2, x3, x5)
row2col_5_in_agaga₅(x1, x2, x3, x4, x5) = row2col_5_in_agaga₂(x2, x4)
if_row2col_5_in_1_agaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_agaga₁(x8)
row2col_5_out_agaga₅(x1, x2, x3, x4, x5) = row2col_5_out_agaga₃(x1, x3, x5)
transpose_aux_3_out_aga₃(x1, x2, x3) = transpose_aux_3_out_aga₂(x1, x3)
ROW2COL_5_IN_AGAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AGAGA₂(x2, x4)
ROW2COL_5_IN_AAAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AAAGA₁(x4)
TRANSPOSE_AUX_3_IN_AGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGA₁(x2)
IF_ROW2COL_5_IN_1_AGAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AGAGA₁(x8)
IF_ROW2COL_5_IN_1_AAAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AAAGA₁(x8)
IF_TRANSPOSE_AUX_3_IN_1_AGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGA₁(x6)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGA₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_5_IN_AGAGA₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2
[]_0 = []_0
ROW2COL_5_IN_AAAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AAAGA₁(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₁(A) -> ROW2COL_5_IN_AAAGA₁(._2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ROW2COL_5_IN_AAAGA₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
transpose_aux₃: (f,b,f)
row2col₅: (f,b,f,b,f) (f,f,f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGA₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_5_IN_AGAGA₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

The argument filtering Pi contains the following mapping:
transpose_aux_3_in_aga₃(x1, x2, x3) = transpose_aux_3_in_aga₁(x2)
._2₂(x1, x2) = ._2
[]_0 = []_0
if_transpose_aux_3_in_1_aga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_aga₂(x3, x6)
row2col_5_in_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_in_aaaga₁(x4)
if_row2col_5_in_1_aaaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_aaaga₂(x6, x8)
row2col_5_out_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_out_aaaga₅(x1, x2, x3, x4, x5)
row2col_5_in_agaga₅(x1, x2, x3, x4, x5) = row2col_5_in_agaga₂(x2, x4)
if_row2col_5_in_1_agaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_agaga₂(x6, x8)
row2col_5_out_agaga₅(x1, x2, x3, x4, x5) = row2col_5_out_agaga₅(x1, x2, x3, x4, x5)
transpose_aux_3_out_aga₃(x1, x2, x3) = transpose_aux_3_out_aga₃(x1, x2, x3)
ROW2COL_5_IN_AGAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AGAGA₂(x2, x4)
ROW2COL_5_IN_AAAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AAAGA₁(x4)
TRANSPOSE_AUX_3_IN_AGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGA₁(x2)
IF_ROW2COL_5_IN_1_AGAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AGAGA₂(x6, x8)
IF_ROW2COL_5_IN_1_AAAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AAAGA₂(x6, x8)
IF_TRANSPOSE_AUX_3_IN_1_AGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGA₂(x3, x6)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGA₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_5_IN_AGAGA₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AGAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

The argument filtering Pi contains the following mapping:
transpose_aux_3_in_aga₃(x1, x2, x3) = transpose_aux_3_in_aga₁(x2)
._2₂(x1, x2) = ._2
[]_0 = []_0
if_transpose_aux_3_in_1_aga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_aga₂(x3, x6)
row2col_5_in_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_in_aaaga₁(x4)
if_row2col_5_in_1_aaaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_aaaga₂(x6, x8)
row2col_5_out_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_out_aaaga₅(x1, x2, x3, x4, x5)
row2col_5_in_agaga₅(x1, x2, x3, x4, x5) = row2col_5_in_agaga₂(x2, x4)
if_row2col_5_in_1_agaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_agaga₂(x6, x8)
row2col_5_out_agaga₅(x1, x2, x3, x4, x5) = row2col_5_out_agaga₅(x1, x2, x3, x4, x5)
transpose_aux_3_out_aga₃(x1, x2, x3) = transpose_aux_3_out_aga₃(x1, x2, x3)
ROW2COL_5_IN_AGAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AGAGA₂(x2, x4)
ROW2COL_5_IN_AAAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AAAGA₁(x4)
TRANSPOSE_AUX_3_IN_AGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGA₁(x2)
IF_ROW2COL_5_IN_1_AGAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AGAGA₂(x6, x8)
IF_ROW2COL_5_IN_1_AAAGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_ROW2COL_5_IN_1_AAAGA₂(x6, x8)
IF_TRANSPOSE_AUX_3_IN_1_AGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGA₂(x3, x6)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 5 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

The TRS R consists of the following rules:

transpose_aux_3_in_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_in_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
row2col_5_in_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B))
if_row2col_5_in_1_aaaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_aaaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga₈(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)) -> row2col_5_out_agaga₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B)
if_transpose_aux_3_in_1_aga₆(R, Rs, underscore, C, Cs, row2col_5_out_agaga₅(R, ._2₂(C, Cs), Cols1, []_0, Accm)) -> transpose_aux_3_out_aga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))

The argument filtering Pi contains the following mapping:
transpose_aux_3_in_aga₃(x1, x2, x3) = transpose_aux_3_in_aga₁(x2)
._2₂(x1, x2) = ._2
[]_0 = []_0
if_transpose_aux_3_in_1_aga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_aga₂(x3, x6)
row2col_5_in_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_in_aaaga₁(x4)
if_row2col_5_in_1_aaaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_aaaga₂(x6, x8)
row2col_5_out_aaaga₅(x1, x2, x3, x4, x5) = row2col_5_out_aaaga₅(x1, x2, x3, x4, x5)
row2col_5_in_agaga₅(x1, x2, x3, x4, x5) = row2col_5_in_agaga₂(x2, x4)
if_row2col_5_in_1_agaga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_row2col_5_in_1_agaga₂(x6, x8)
row2col_5_out_agaga₅(x1, x2, x3, x4, x5) = row2col_5_out_agaga₅(x1, x2, x3, x4, x5)
transpose_aux_3_out_aga₃(x1, x2, x3) = transpose_aux_3_out_aga₃(x1, x2, x3)
ROW2COL_5_IN_AAAGA₅(x1, x2, x3, x4, x5) = ROW2COL_5_IN_AAAGA₁(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₅(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA₅(Xs, Cols, Cols1, ._2₂([]_0, A), B)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ROW2COL_5_IN_AAAGA₁(A) -> ROW2COL_5_IN_AAAGA₁(._2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ROW2COL_5_IN_AAAGA₁}.